home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / main_2.06.2 < prev    next >
Text File  |  1992-04-03  |  16KB  |  527 lines
  1. %%% MAIN
  2. %%% version 2.00.0 (based on main_19.4)
  3. %%%   added equality transformation
  4. %%% version 2.00.1
  5. %%%   added equality rewriting
  6. %%% version 2.00.3
  7. %%%   changed "equality_rewriting" to "auto_orient"
  8. %%%   added "outrwr", added "outrwt", added "outtreq", and "pullout_constants"
  9. %%% version 2.00.5
  10. %%%   saved rewrite rules across sessions
  11. %%% version 2.00.6
  12. %%%   added user specified rewrite rules and orderings
  13. %%% version 2.00.8
  14. %%%   added lexicographic path ordering
  15. %%% version 2.01.9
  16. %%%   optimized term rewriting
  17. %%% version 2.03.4
  18. %%%   incorporated changes made to clin V1 between 7/31/90 and 10/18/90 which
  19. %%%     are visible externally -- changes to comments, predicate names, and
  20. %%%     variable names are not incorporated
  21. %%% version 2.04.0
  22. %%%   logically erased nuclei while hyper-linking
  23. %%%   saved input clauses between sessions same as clin 1
  24. %%% version 2.04.1
  25. %%%   determined maximum number of non-ground literals in a clause each round
  26. %%%     (required for equality transform)
  27. %%% version 2.04.4
  28. %%%   when replacing and rewriting, perform replacement/rewrite repeatedly
  29. %%%     until no change
  30. %%% version 2.04.5
  31. %%%   added restricted_rewrite to control whether restricted or unrestricted
  32. %%%     rewriting of equations is used
  33. %%%   added equality_transform_by_round flag
  34. %%%   added safe_early_priority_test flag
  35. %%%   added early_unit_subsumption flag
  36. %%%   added early tautology test
  37. %%%   added small_proof_nucleus_bound
  38. %%% version 2.04.6
  39. %%%   added fixed_priority
  40. %%%   added start_priority_bound
  41. %%%   fixed bug in code which determines if another round of hyper-linking is
  42. %%%     required
  43. %%% version 2.04.8
  44. %%%   added group_detection
  45. %%% version 2.05.0
  46. %%%   don't select a support strategy unless there is a new clause or an
  47. %%%     existing clause has modified the appropriate support
  48. %%%   checked for duplicate partial instances
  49. %%% version 2.05.1
  50. %%%   added clause splitting
  51. %%%   added gensym
  52. %%% version 2.05.2
  53. %%%   modified the top level structure of clin
  54. %%% version 2.05.3
  55. %%%   added support for Quintus Prolog
  56. %%% version 2.05.4
  57. %%%   added banner to Quintus version
  58. %%%   fixed bug which prevented clause_splitting option from being printed
  59. %%% version 2.05.5
  60. %%%   added equational rewriting
  61. %%% version 2.05.6
  62. %%%   changed early unit subsumption to equality early unit subsumption
  63. %%%   added new early unit subsumption
  64. %%%   added print after clause generation
  65. %%% version 2.05.8
  66. %%%   renamed assign/2 to assign_cmd/2 for compatibility with Quintus Prolog 3
  67. %%%   added priority_bound_increment
  68. %%% version 2.06.0
  69. %%%   added clause_generation_loop flag
  70. %%%   added save_rewrite_rules
  71. %%% version 2.06.1
  72. %%%   added constrained rewriting
  73. %%%   added save_unrestricted_normal_form
  74. %%% version 2.06.2
  75. %%%   fixed duplicate setting of inifinity defaults
  76. %%%   added fast_priority_update
  77. %%%   added duplicate_partial_instance_test
  78. %%%   added precompute_constraints
  79. %%%   added restricted_equality_transform
  80. %%%   cached lexicographical path ordering
  81. %%%   added index and size bound to cached_rewrite
  82. %%%   added size bound to cached_constraint_consistent
  83. %%%   added size bound to cached_constrained_term_order and
  84. %%%     cached_constrained_term_order_complete
  85. %%%   cached constrained subterm rewrites
  86. %%%   added cache_size
  87. %%%
  88. %%% This section contains the main procedure.
  89. %%%
  90.  
  91. %%% Prove the theorem in File.
  92. %%% If user_control is specified, then File is the problem to be solved.
  93. %%% Otherwise, File may be the problem itself or a file containg
  94. %%%    a list of problems depending if batch mode is used.
  95.      prove(_) :-
  96.     quintus_banner,
  97.     set_infinity_defaults,
  98.     fail.
  99.      prove(File) :-             
  100.     user_control, !,
  101.     prove_1(File), !, fail.
  102.      prove(File) :-             
  103.     xvisor(File), !, fail.
  104.  
  105. %%% prove_1 fails in the following cases: 
  106. %%%     Read erroneous commands in interp.
  107. %%%     No user support clauses if user support strategy is specified
  108. %%%    in interp.
  109. %%% 
  110. %%% Clear the database to avoid the interference of the assertions from
  111. %%%    the previous run.
  112. %%% Call interpreter to assert clauses with internal format.
  113. %%% If automatic control, check if the input is a horn set.
  114. %%% Try to solve the given problem.
  115. %%% Print out statistics for the tried problem.
  116. %%% Reset flags due to horn set.
  117. %%% If user_control, reset options that are set in the spec. of the problem.
  118.      prove_1(Prob) :-             
  119.     not(not(clear_database)),
  120.     assert(file_name(Prob)),
  121.     !,
  122.     interp,
  123.     not(not(set_real_time_limit)),
  124.     check_horn_set(D),
  125.     try,
  126.     not(not(summary)),
  127.     reset_by_horn_set(D),
  128.     not(not(postproc)), !.
  129.  
  130. %%% CLEAR DATABASE
  131. %%%
  132. %%% Clear the database so that the remanants from the previous problem won't
  133. %%% affect the proof of the current problem.
  134.      clear_database :-            % clearing the database.
  135.     abolish(cached_constrained_term_order,5),
  136.                     % cached constrained term order data.
  137.     abolish(cached_constrained_term_order_complete,4),
  138.                     % cached constrained term order data.
  139.     set_counter(cached_constrained_term_order_count,0),
  140.         abolish(cached_constraint_consistent,4),
  141.                     % cached constraint consistency data.
  142.     set_counter(cached_constraint_consistent_count,0),
  143.         abolish(cached_term_order,5),   % cached term order data.
  144.     set_counter(cached_term_order_count,0),
  145.         abolish_rewrite_caches,         % cached rewrite data
  146.         abolish(cps_A,5),         % data structure for spc.
  147.         abolish(cps_I,6),         % data structure for spc.
  148.         abolish(cps_O,5),         % data structure for spc.
  149.         abolish(cps_U,5),         % data structure for spc.
  150.         abolish(cps_V,5),         % data structure for spc.
  151.     abolish(current_num,2),         % get_num data
  152.     abolish(sp_size,1),          % small proof size.
  153.     abolish(db_erased,1),        % release memory.
  154.         abolish(dont_use_rewrite_rule,1),% temporarily suspended equation
  155.     abolish(du,2),            % temporary assertions in unit simp.
  156.     abolish(error,1),        % error indication.
  157.     abolish(file_name,1),        % file name.
  158.     abolish(in_fms,2),        % release memory.
  159.     abolish(last_hypermatch_time,1),% time spent on last hyper-matching.
  160.     abolish(lit_G,4),        % general literal list.
  161.     abolish(lit_S,4),        % literal list from supported clauses.
  162.     abolish(lit_N_G,5),        % literal list for replacements.
  163.     abolish(lit_N_V,5),        % literal list for replacements.
  164.     abolish(lit_ST_G,5),        % literal list for replacements.
  165.     abolish(lit_ST_V,5),        % literal list for replacements.
  166.     abolish(lit_U,3),        % literal list from unit clauses.
  167.     abolish(logically_erased,2),    % logically erased clauses.
  168.     abolish(no_user_clauses,0),      % set in interp.
  169.     abolish(nonvar_depth_weight,2), % depth weight for non-variable.
  170.     abolish(nonvar_size_weight,2),  % size weight for non-variable.
  171.     abolish(nu,1),            % used in duplicate deletion.
  172.     abolish(num,1),            % for numbering printed stuff.
  173.     abolish(number_inclauses,1),    % number of input clauses.
  174.     abolish(ou,2),            % temporary assertions in unit simp.
  175.     abolish(out_model_rc,0),    % clear flag for pc prover.
  176.     abolish(part_inst,4),        % partial instances
  177.     abolish(pc_time,1),        % record total pc prover time.
  178.     abolish(priority_bound_increment,1), % priority_bound_increment.
  179.     abolish(proof_type,1),        % proof type.
  180.     abolish(prove_result,1),    % record the proof result.
  181.     abolish(replace_rule_1,5),    % replace rules.
  182.     abolish(replace_rule_2,5),    % replace rules.
  183.     abolish(rwe,1),            % the rewrite equivs.
  184.     abolish(rwo,1),            % the rewrite orderings.
  185.     abolish(rwr,4),            % the rewrite rules.
  186.     abolish(sent_HM,1),        % temp. clauses in hyper-matching.
  187.     abolish(sent_T,1),        % temp. clauses in hyper-matching.
  188.     abolish(sent_c,1),        % temp. clauses.
  189.     abolish(session_no,1),        % store session no.
  190.     abolish(start_time,1),        % starting time of the proof.
  191.     abolish(uparg,6),        % used in duplicate deletion.
  192.     abolish(updated_arguments,0),    % used in duplicate deletion.
  193.     abolish(user_support,1),    % user support indicator.
  194.     abolish(user_supportset,1),    % user support list.
  195.     abolish(var_depth_weight,2),    % depth weight for all variables.
  196.     abolish(var_size_weight,2),     % size weight for all variables.
  197.     abolish(wu_bound,1),        % current hyper-match workunit bound.
  198.     session_deletions, !.        % deletions done before a session.
  199.  
  200. % delete assertions of the previous session.
  201.      session_deletions :- 
  202.         abolish_rewrite_caches,         % cached rewrite data
  203.     abolish(complete_supp,1),    % support round strategy having 
  204.                     % unchanged assertions.
  205.     abolish(current_support,1),    % recording current support strategy.
  206.         abolish(group_descr,3),         % group descriptions.
  207.     abolish(num_supp,1),        % Nth support strategy in support list.
  208.     abolish(oldsentC,3),        % old clauses.
  209.     abolish(oldsentC1,1),        % old clauses.
  210.     abolish(over_litbound,0),    % indicator, too many literals.
  211.     abolish(over_numvars,0),    % indicator, too many variables.
  212.     abolish(over_priohm,0),        % indicator, over priority.
  213.     abolish(over_relevance,0),    % indicator, over relevance.
  214.     abolish(prio_wu,3),        % counter for different priorities.
  215.     abolish(round_no,1),        % current round number.
  216.     abolish(round_time,2),        % the time at end of each round.
  217.     abolish(total_numhm,1),        % total number of hyper-matches so far.
  218.     abolish(total_wu,1).        % total number of hyper-matches so far.
  219.  
  220. %%% Set real time limit.
  221. %%% Default is no change.
  222.      set_real_time_limit :-
  223.     \+ user_control,
  224.     time_limit(X),
  225.     set_real_time_limit(X), !.
  226.      set_real_time_limit :-
  227.     time_limit(X),
  228.     set_real_time_limit(X), !.
  229.  
  230.      set_real_time_limit(T) :-
  231.     time_limit_coef(F),
  232.     abolish(real_time_limit,1),
  233.     Temp is F*T,
  234.     floor(Temp,RTL),
  235.     assert(real_time_limit(RTL)).
  236.      set_real_time_limit(T) :-
  237.     abolish(real_time_limit,1),
  238.     assert(real_time_limit(T)).
  239.  
  240. %%% If user_control, then no effect.
  241. %%% If the input is Horn-set, then set delete_all_instances.
  242.      check_horn_set(1) :-
  243.     user_control, !.
  244.      check_horn_set(X) :-
  245.     check_horn_set_2(X),
  246.     check_horn_set_1.
  247.  
  248.      check_horn_set_1 :-
  249.     sent_C(cl(_,_,by(Cn1,_,_,_,_),_,_,_,_,_,_)),
  250.     check_horn_clause(Cn1), !.    % succeed if not horn set.
  251.      check_horn_set_1 :-        % If horn set.
  252.     set(delete_all_instances).
  253.  
  254.      check_horn_clause(Cn1) :-        % fail if horn clause.
  255.     horn_clause(Cn1),
  256.     !,
  257.     fail.
  258.      check_horn_clause(_).        % If not horn set.
  259.  
  260. %%% If delete_all_instances is set initially, return 1, otherwise 0.
  261.      check_horn_set_2(1) :-
  262.     delete_all_instances, !.
  263.      check_horn_set_2(0).
  264.  
  265. %%% Reset the delete_all instances if necessary.
  266. %%% If delete_all_instances is not set initially, delete it. 
  267.      reset_by_horn_set(0) :-
  268.     clear(delete_all_instances), !.
  269.      reset_by_horn_set(_).
  270.  
  271. %%% 
  272. %%% REPORT OUT
  273. %%%
  274. %%% Report the summary of the proof.
  275.      summary :-
  276.     cputime(T),
  277.     nl,
  278.     write_line(5,'SUMMARY:'),
  279.     report_file,
  280.     settings,
  281.     check_print_pc_model_rc,
  282.     report_proof(T), !.
  283.  
  284. %%% Print out filename and number of input clauses of the underlying problem.
  285.      report_file :-
  286.     file_name(File),
  287.     write_line(5,'Underlying-File: ',File),
  288.     number_inclauses(IN),
  289.     write_line(5,'Number-Of-Input-Clauses: ',IN).
  290.  
  291. %%% Print out options set for the underlying problem.
  292.      settings :-
  293.     member(X,[
  294.         outCacg,
  295.         outCagen,
  296.         outCahl,
  297.         outCainst,
  298.         outCasimp,
  299.         outcsplit,
  300.         outfls,
  301.         outhl,
  302.         outhllits,
  303.         outpc,
  304.         outpcin,
  305.         outrwr,
  306.         outrwt,
  307.         outtreq,
  308.         cache_size(_),
  309.         clause_splitting(_),
  310.         depth_coef(_),
  311.         literal_coef(_),
  312.         max_no_clauses(_),
  313.         relevance_bound(_),
  314.         relevance_coef(_),
  315.         size_coef(_),
  316.         start_no_clauses(_),
  317.         start_no_clauses_coef(_),
  318.         support_list(_),
  319.         term_ordering(_),
  320.         time_limit(_),
  321.         time_limit_coef(_),
  322.         time_limit_multiple(_),
  323.         back_literalbound(_),
  324.         small_proof_nucleus_bound(_),
  325.         small_proof_size_bound(_),
  326.         for_literalbound(_),
  327.         literal_bound(_),
  328.         user_literalbound(_),
  329.         start_priority_bound(_),
  330.         priority_bound_increment(_),
  331.         start_wu_bound(_),
  332.         restricted_equality_transform(_),
  333.         auto_orient,
  334.         clause_generation_loop,
  335.         constrained_rewriting,
  336.         count_all_literals,
  337.         delete_all_instances,
  338.         delete_nf_instances,
  339.         do_hyper_linking,
  340.         duplicate_partial_instance_test,
  341.         early_tautology_test,
  342.         early_unit_subsumption,
  343.         equality_early_unit_subsumption,
  344.         equality_transform,
  345.         equality_transform_by_round,
  346.         equational_rewrite,
  347.         fast_priority_update,
  348.         fixed_priority,
  349.         ground_disting_after_match,
  350.         ground_restriction,
  351.         ground_substitution,
  352.         group_detection,
  353.         hl_literal_reordering,
  354.         include_original_clause,
  355.         precompute_constraints,
  356.         pullout_constants,
  357.         realfls,
  358.         replace_literal_reordering,
  359.         replacement,
  360.         restricted_rewrite,
  361.         safe_early_priority_test,
  362.         save_unrestricted_normal_form,
  363.         save_rewrite_rules,
  364.         simple_small_proof_check,
  365.         size_by_clause,
  366.         slidepriority,
  367.         small_proof_check,
  368.         small_proof_check_all,
  369.         spc_literal_reordering,
  370.         sum_of_measures,
  371.         super_batch,
  372.         tautology_deletion,
  373.         unit_resolution,
  374.         user_control
  375.     ]),
  376.     call(X),
  377.     write_line(15,'',X),
  378.     fail.
  379.      settings.
  380.  
  381. %%% Print out information about the try of the underlying problem.
  382.      report_proof(T) :-
  383.     report_trystatus,
  384.     report_proof_type,
  385.     report_session_round_no,
  386.          report_number_C_space,
  387.     report_PrWu_bounds,
  388.     report_pc_time,
  389.     report_total_time(T).
  390.  
  391. %%% What is the status of the try.
  392.      report_trystatus :-
  393.     tab(25),write('What: '),
  394.     prove_result(PR),
  395.     write(PR),nl,!.
  396.  
  397. %%% If the underlying problem was proved, how it was proved.
  398. %%% If was proved by small proof checker, print out small proof size.
  399.      report_proof_type :-
  400.     report_proof_type_1(PT),
  401.     report_proof_type_2(PT).
  402.  
  403.      report_proof_type_1(PT) :-
  404.     proof_type(PT),
  405.     write_line(25,'Proof-Type: ',PT), !.
  406.      report_proof_type_1(_).
  407.  
  408.      report_proof_type_2(PT) :-
  409.     PT == 'SP',
  410.     sp_size(N1), 
  411.     write_line(25,'Small_Proof_Size: ',N1), !.
  412.      report_proof_type_2(_).
  413.  
  414. %%% Print out how many rounds in the final session.
  415.      report_session_round_no :-
  416.     session_no(SessionNo),
  417.     round_no(RoundNo),
  418.     write_line(25,'Number-Of-Sessions: ',SessionNo),
  419.     write_line(25,'Number-Of-Rounds: ',RoundNo).
  420.  
  421. %%% Print out how many hyper-matches at the end.
  422.      report_number_C_space :-
  423.     get_C_number_space(0,0,M,S),
  424.     write_line(25,'Number-Of-Clauses-Retained: ',M),
  425.     write_line(25,'Space-Used-In-Units: ',S).
  426.               
  427.      get_C_number_space(M1,S1,M2,S2) :-
  428.     retract(sent_C(cl(Z,_,_,_,_,_,_,_,_))),
  429.     MM is M1 + 1,
  430.     SS is S1 + Z,
  431.     !, get_C_number_space(MM,SS,M2,S2).
  432.      get_C_number_space(M,S,M,S).
  433.  
  434. %%% Print out information about sliding priority.
  435.      report_PrWu_bounds :-
  436.     slidepriority,
  437.         report_PrWu_bounds_1, !.
  438.      report_PrWu_bounds.
  439.  
  440.      report_PrWu_bounds_1 :-
  441.     priority_bound(PrioBound),
  442.     write_line(25,'Priority-Bound: ',PrioBound),
  443.     wu_bound(WUBound),
  444.     write_line(25,'Work-Unit-Bound: ',WUBound), !. 
  445.      report_PrWu_bounds_1.
  446.  
  447. %%% Print out total PC time used.
  448.      report_pc_time :-
  449.     tab(25),write('PC-Prover-Time: '),
  450.          report_pc_time_1.
  451.  
  452.      report_pc_time_1 :-
  453.     pc_time(PCTIME), write(PCTIME), nl, !.
  454.      report_pc_time_1 :-
  455.     write(0), nl.
  456.  
  457. %%% Print out total CPU time used.
  458.      report_total_time(T) :-
  459.     start_time(Start_Time),
  460.     Used_Time is T - Start_Time,
  461.     write_line(25,'Total-Time: ',Used_Time).
  462.  
  463. %%% Print out model or relevant clauses to the proof by PC prover.
  464.      check_print_pc_model_rc :-
  465.     outpc,
  466.     print_pc_model_rc.
  467.      check_print_pc_model_rc.
  468.  
  469.      print_pc_model_rc :-
  470.     prove_result('satisfiable'),
  471.     print_pc_model_rc_1, !.
  472.      print_pc_model_rc :-
  473.     proof_type('PC'),
  474.     print_pc_model_rc_1, !.
  475.      print_pc_model_rc.
  476.     
  477.      print_pc_model_rc_1 :-
  478.     compute_fms(FMS),
  479.     assert(out_model_rc),
  480.     run_pc_mr(FMS),
  481.     abolish(out_model_rc,0), !.
  482.  
  483.      run_pc_mr(FMS) :-
  484.     outpcin,
  485.     write_line(5,'Input to PC:'),
  486.     print_clause_list(FMS),
  487.     intell_pc(FMS,_).
  488.      run_pc_mr(FMS) :- 
  489.     intell_pc(FMS,_).
  490.  
  491. %%% Postprocess commands in input file.
  492.      postproc :-
  493.     user_control,
  494.     file_name(File),
  495.     seeing(Input),
  496.     see(File),
  497.     read_till_end_input,
  498.     postproc_1,
  499.     seen,   
  500.     see(Input), !.
  501.      postproc.
  502.  
  503. %%% Read input until the command following end_of_input.
  504.      read_till_end_input :-
  505.     repeat,
  506.         read(Term),
  507.         Term == 'end_of_input'.
  508.  
  509.      postproc_1 :-
  510.     read(Term),
  511.     Term \== 'end_of_file',
  512.     postproc_1(Term), !,
  513.     postproc_1.
  514.      postproc_1.
  515.  
  516. %%% Perform actions according to the command.
  517.      postproc_1(set(X)) :-
  518.     set(X).
  519.      postproc_1(clear(X)) :-
  520.     clear(X).
  521.      postproc_1(assign(X,V)) :-
  522.     assign_cmd(X,V).
  523.      postproc_1(delete(X,V)) :-
  524.     delete(X,V).
  525.      postproc_1(Term) :-
  526.     write_line(5,'ERROR: Wrong input -> ',Term), !, fail.
  527.